$\forall$${\it es}$:ES, $a$, $b$:E.
\\[0ex]($\uparrow$isrcv($a$))
\\[0ex]$\Rightarrow$ ($\uparrow$isrcv($b$))
\\[0ex]$\Rightarrow$ (lnk($a$) = lnk($b$) $\in$ IdLnk)
\\[0ex]$\Rightarrow$ (sender($a$) $<$ sender($b$))
\\[0ex]$\Rightarrow$ ($a$ $<$ $b$)